T:Type, L:T List. null(L)  (f:(T). x:T. (x  L)  (t:. t':. tt' & f(t') = x)) 

latex

Definitions	S  T, Top, t  T, P  Q, x:A. B(x), Prop, x:A. B(x), Y, True, ||as||, False, a  b, , A, , P & Q, {T}, SQType(T), P  Q, P  Q, Dec(P), if b t else f fi, false, true, null(as), b, AB, , A & B, (x  l)
Lemmas	top wf, null wf3, assert wf, not wf, assert of null, not functionality wrt iff, decidable assert, non neg length, length wf1, select wf, rem bounds 1, nat wf, l member wf, nequal wf, div rem sum, divide wfa, rem invariant, div bounds 1, rem base case, le wf